In 1965, Gordon Moore suggested the number of transistors in devices will approximately double every two years. This observation, widely known as Moore's Law, is still valid today. The pace of innovation of process technology has been nothing short of remarkable. The industry is currently working on 65 and 45 nanometer designs, enabling billion transistor devices. The size of the industry is equally impressive. The Semiconductor Industry Association estimated that sales for 2006 for integrated circuit devices would be over $207 Billion US and over $262 Billion by 2008. There seems to be no end to the demand for new and more complex products requiring integrated circuits.
Engineers use Electronic Design Automation (EDA) tools to develop and manufacture these devices. The complexity of millions and soon billions of transistors is clearly a task for computer-aided automation. In 2004, the market for these software tools was estimated to be over $4 Billion US and expected to grow at an annual rate of 10%.
These EDA tools are used to implement the design objectives from the initial abstract form of the circuit behavior to a final database which foundries use to manufacture devices. As a result of the increasing complexity, verifying that the design intent is faithfully implemented is becoming the dominant task within the overall project. The cost to design a new device is subject to many factors such as; re-use of IP (Intellectual Property) blocks, process technologies, complexity, and company specific overheads. In the International Technology Roadmap for Semiconductors (ITRS) 2005 Report on Design, the cost of a 6.5 million logic gate System on Chip was estimated to be close to $20 millions US.
Therefore, producing error-free Integrated Circuits (ICs) is of paramount importance in the semiconductor industry. In some cases the importance is of an economic nature, as product recalls and loss of market shares are but some of the consequences of providing faulty circuits. In military and aerospace applications, the consequences can be more direct especially when human lives enter the equation. Examples of defects in ICs range from satellite and rocket malfunctions, to glitches and failures in consumer applications. One well-known case is the floating-point error found on early models of the Pentium processor by Intel. This “bug”, known as the FDIV bug was not a fabrication or manufacturing defect, but rather a functional error in the design of the division algorithm.
Verification aims to ensure that a circuit design behaves according to its intended specification. Verification deals with functional errors in circuit designs, in contrast to testing which deals with the detection of fabrication errors in ICs. In today's complex hardware digital circuit designs, verification typically requires more effort than the actual design phase itself. The predominant current verification methodology is based on an ad-hoc simulation-based approach, sometimes aided with coverage metrics. The design is verified by building a series of models, selecting test vectors, simulation and troubleshooting the resulting errors. This can be considered a post design approach. Although a large number of simulations can be run, the effort spent in fixing the bugs does not resolve the question of whether the design is faithful. A heavy burden is placed on design teams to prioritize which design areas need special attention and to identify events which could trigger a catastrophic failure. For those reasons, the ITRS suggests that without new techniques, verification will be a barrier for progress in the industry.
Amongst others, one technique, Assertion Based Verification (ABV) is emerging as a powerful approach for designers. This approach allows for a precise description of the expected behavior of the system to be modeled using temporal logic. Deviation from the expected behavior can be captured during simulations or by formal methods. Recently, the Institute of Electrical and Electronics Engineers (IEEE) adopted two languages for assertion specification; Property Specification Language (PSL) developed by IBM™ and Accellera™ (IEEE-1850) and System Verilog™ (IEEE-1800), accelerating its adoption.
After errors have been identified, the next step is to debug the design. Like finding the proverbial needle in the haystack, debugging increasingly complex devices can easily become a roadblock to delivering the end product on time.
Other vendors' products support assertions in multiple languages and allow for circuit emulation. These systems are substantial investments and form part of each company's comprehensive EDA portfolio.
In the emerging DFD (Design For Debug) space, companies are promoting a range of solutions. One such solution enables the designers to select an instrumentation structure, which can be synthesized and used post fabrication for debugging.
Hardware verification aims to ensure that a design fulfills its given specification by either formal or dynamic (simulation based) techniques. As one facet of Assertion-Based Design, Assertion-Based Verification (ABV) is quickly emerging as the dominant methodology for performing hardware verification in practice. Using temporal logic, a precise description of the expected behavior of a design is modeled, and any deviation from this expected behavior is captured by simulation or by formal methods. Hardware assertions are typically written in a verification language such as PSL (Property Specification Language) or SVA (SystemVerilog Assertions). When used in dynamic verification, a simulator monitors the Device Under Verification (DUV) and reports when assertions are violated. Information on where and when assertions fail is an important aid in the debugging process, and is the fundamental reasoning behind the ABV methodology. Assertion-Based Design practices also advocate the use of assertions as part of the design effort, when used as a formal documentation language. Assertions even go beyond design and verification, when used with a checker generator. In such cases, circuit-level checkers can be produced to create permanent circuitry that is to be added to a design, in order to perform silicon monitoring for self-test and diagnostic purposes, during the lifespan of the IC.
As circuits become more complex, hardware emulation is becoming an increasingly important asset for verification. Hardware emulation achieves the traditional dynamic verification goals by loading and executing the circuit on a reprogrammable hardware substrate, typically on an array of programmable logic devices. Once implemented in hardware, the emulator fully exploits the inherent circuit parallelism, as opposed to performing a serial computation in a simulation kernel. Furthermore, when design errors are found during emulation, additional information from the assertion checkers should be used to point to the source of the problem.
Assertion languages allow the specification of expressions that do not lend themselves directly to hardware implementations. Such languages allow complex temporal relations between signals to be stated in a compact and elegant form. In order to consolidate assertion-based verification and emulation, a checker generator is used to generate hardware assertion checkers. A checker generator is the tool that transforms assertions into assertion monitor-circuits (checkers), directly usable in hardware emulation. The overall operation of a checker generator is illustrated in FIG. 8, using a simple example scenario. A checker generator allows the flexibility of automatically generating custom monitor circuits from any assertion statement. Coding checkers by hand can be a tedious and error-prone task. In certain cases, a single PSL statement can imply tens or even hundreds of lines of RTL code in the corresponding checker.
Individual assertions, once converted to circuit form, are also referred to as assertion circuits. These checker circuits are typically expressed in a Hardware Description Language (HDL). An assertion checker is a circuit that captures the behavior of a given assertion, and can be included in the DUV for in-circuit assertion monitoring.
The concept of checker generators for PSL was pioneered by IBM™ and their FoCs tool as described in AlphaWorks, FoCs Property Checkers Generator, version 2.04, available on www.alphaworks.ibm.com/tech/FoCs, 2007. The original assertion language that served as the foundation for PSL was actually developed by IBM™ and was called Sugar™. The FoCs tool was originally intended for simulation use; however, the circuit checkers that were produced could also be synthesized in hardware.